Nuprl Lemma : qle_functionality_wrt_implies
11,40
postcript
pdf
a
,
b
,
c
,
d
:
. (
b
a
)
c
d
{
b
c
a
d
}
latex
Definitions
t
T
,
{
T
}
,
P
Q
,
x
:
A
.
B
(
x
)
,
a
b
,
Lemmas
rationals
wf
,
qge
wf
,
qle
wf
,
qle
transitivity
qorder
origin
a, b, c, d:
. (b 
a) 
c 
d {b c a d} a, b, c, d:. (b a) c d {b c a d} 
T Qx:A. B(x) b